T:Type, l1, l2, l3:T List. l1  l2 @ l3  ||l1||||l2||  l1  l2 

latex

Definitions	l1  l2, t  T, P  Q, x:A. B(x), P  Q, P & Q, P  Q, x:A. B(x), False, A, AB, P  Q, as @ bs, ||as||
Lemmas	le wf, iseg wf, append wf, iseg append iff, length wf1, length append